Inference at * 1 
Iof proof for Lemma do-apply-p-filter:



1. T : Type
2. P : T
3. f : x:T. Dec(P(x))
4. x : T
  (isl(case f(x) of inl(p) => inl x  | inr(p) => inr p ))
   (outl(case f(x) of inl(p) => inl x  | inr(p) => inr p ) = x) 

latex

 by ((((GenConcl f(x) = z) 
CollapseTHENA (Auto))) 
CollapseTHEN (((D (-2)) 
CollapseTHEN (((
CoReduce 0) 
CollapseTHEN (Auto)))))) 

latex

Co.

Definitions	s = t, Dec(P), x(s), f(a), , x:AB(x), P  Q, left + right, True, b, P  Q, x:A. B(x), t  T, False
Lemmas	decidable wf, true wf, false wf